COMMENT ⊗   VALID 00003 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	THE FIRST EXAMPLE: PLANE GEOMETRY PROBLEM
 00004 00003	EXAMPLE TWO: AN AXIOMATIZATION OF THE MONKEY AND BANANA PROBLEM
 00006 ENDMK
⊗;
THE FIRST EXAMPLE: PLANE GEOMETRY PROBLEM

The input:

VAR: x,y,z,u,v,w;
PRE_PRED: T,C,S,A;

A1: S(x,y,y,x);
A2: S(u,v,x,y)⊃S(x,y,u,v);
A3: S(u,v,x,y)⊃S(v,u,x,y);
A4: T(x,y,z)⊃T(y,z,x);
A5: T(x,y,z)⊃T(y,x,z);
A6: C(u,v,w,x,y,z)⊃(A(u,v,w,x,y,z)∧A(v,u,w,y,x,z)∧A(u,w,v,x,z,y));
A7: (T(u,v,w)∧T(x,y,z)∧S(u,v,x,y)∧S(v,w,y,z)∧S(u,w,x,z))⊃
            C(u,v,w,x,y,z);
THM:(T(x,y,z)∧S(x,z,y,z))⊃A(z,x,y,z,y,x);;

The following is the output:


CHOICE-STRATEGY-IS: 		The strategies used.
ANCESTRY∧SUPPORT[THM];

EDIT-STRATEGY-IS: 
DEPTH[1]∨LENGTH[5];

ELAPSED-TIME =43351		The time in milliseconds.

 
NIL 1 5				The refutation.
1 S(THM2,THM3,THM3,THM1);3 4
3 S(THM3,THM1,THM2,THM3);5 6
4 S(z,u,x,y)⊃S(x,y,z,u);A2
5 S(y,x,z,u)⊃S(x,y,z,u);A3

In this example 243 clauses were generated and 173 remained in memory when
the refutation was found

EXAMPLE TWO: AN AXIOMATIZATION OF THE MONKEY AND BANANA PROBLEM

	The input:

VAR: x,y,z;
PRE_OP:m,b,c,f;PRE_PRED:r,a,cl,o,u,t,i,mv,cb;

AXIOM:
a(x)∧cl(x,y)⊃r(x,y);
o(x,y)∧u(y,b)∧t(y)⊃cl(x,b);
i(x)∧i(y)∧i(z)∧mv(x,y,z)⊃(cl(z,f)∨u(y,z));
cb(x,y)⊃o(x,y);
a(m);
t(c);
i(m);
i(b);
i(c);
mv(m,c,b);
¬cl(b,f);
cb(m,c);
THM: r(m,b);
;

	The output:


CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THM];

EDIT-STRATEGY-IS: 
DEPTH[1]∨LENGTH[5];

ELAPSED-TIME =2016

NIL 1 2
1 ¬(cb(m,x)∧(mv(y,x,b)∧(i(y)∧(i(x)∧t(x)))));3 4
2 mv(m,c,b);AXIOM
3 ¬(cb(m,x)∧(t(x)∧u(x,b)));5 6
4 mv(z,x,y)∧(i(z)∧(i(x)∧i(y)))⊃cl(y,f)∨u(x,y);AXIOM
5 ¬(t(x)∧(o(m,x)∧u(x,b)));7 8
6 cb(x,y)⊃o(x,y);AXIOM
7 ¬cl(m,b);9 10
8 t(y)∧(o(x,y)∧u(y,b))⊃cl(x,b);AXIOM
9 ¬r(m,b);THM

Here 27 clauses were generated but only 12 remained in memory when 
the refutation was found.